1. $A$ : Type
\\[0ex]2. $B$ : Type
\\[0ex]3. $f$ : $A$$\rightarrow$$B$
\\[0ex]4. $\forall$$a_{1}$, $a_{2}$:$A$. ($f$($a_{1}$) = $f$($a_{2}$)) $\Rightarrow$ ($a_{1}$ = $a_{2}$)
\\[0ex]5. $\exists$$f_{1}$:$B$$\rightarrow$$A$. ($\forall$$b$:$B$. $f$($f_{1}$($b$)) = $b$)
\\[0ex]$\vdash$  $\exists$$g$:$B$$\rightarrow$$A$. InvFuns($A$;$B$;$f$;$g$)